Satisfiability (SAT) is a computationally-difficult problem which is central to many computer-aided design (CAD) and test applications. The SAT problem may be characterized as follows: given a boolean function F(x.sub.1, x.sub.2, . . . x.sub.n), find an assignment of binary values to the variables x.sub.1, x.sub.2, . . . x.sub.n, such that F is set to 1, or prove that no such assignment exists. Typically, F is expressed as a product-of-sums, which is also called conjunctive normal form (CNF). In applications involving combinational circuits, the variables x.sub.j may represent primary inputs (PIs) of a given circuit, while F represents the primary output (PO) of that circuit. CAD and test applications that can be characterized as a SAT problem include, for example, timing verification, routing and routability analysis, fault diagnosis, logic synthesis and logic verification. SAT is also related to automatic test pattern generation (ATPG) algorithms, as it can be viewed, e.g., as the problem of generating a test for a stuck-at-0 fault on a PO. An important component in ATPG is the so-called line justification problem, which deals with setting an internal signal to a given value, and corresponds to SAT on a subcircuit. Many other computationally-difficult problems, such as graph coloring, scheduling, theorem proving and constraint satisfaction problems, have also been mapped to SAT problems.
A significant drawback often associated with SAT problems is the amount of computation time required for their solution. Even with the most advanced SAT algorithms, difficult problems, such as, for example, those involving complex very-large-scale integration (VLSI) circuits, can require many hours of computation using powerfill computers. A number of recently-developed techniques have attempted to simplify the SAT computation process through the use of reconfigurable hardware. Reconfigurable hardware is used in adaptive computing and other applications to implement logic circuit functions. A given set of reconfigurable hardware, which may be based on field programmable gate arrays (FPGAS) or other similar programmable logic devices, can be reconfigured so as to provide different logic functions at different times, thereby in effect providing the functionality of a complex circuit which would otherwise require substantially more hardware. Circuits implemented in reconfigurable hardware to facilitate SAT computation are referred to as "satisfiers." Although existing satisfiers and other conventional techniques and devices have produced reductions in the computational complexity of SAT algorithms, additional improvements are needed to provide further improvements in the efficiency of the many CAD, test and other types of applications that utilize SAT.